Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
形式方法遇上大语言模型：高级AI系统的合规审计、监控与干预
🧭 Agent 行为合规监控 · 形式方法 ★ 深度解读
University of Toronto · Vector Institute
利用LTL进展将时序合规监控拆解为LLM标注+形式推理，效果远超LLM直接评判，并实现预测性干预
📌 工作参考价值（4 点）
- 用 LTL 形式化业务规则，监控 Agent 行为：电商场景中复杂的时序约束（如“必须先确认支付再发货，且发货前需人工审核大额订单”）可直接用 LTL 表达，结合 TRAC 对客服机器人、推荐流程或供应链Agent进行实时合规检查。
- 小模型标注 + 形式逻辑推理 > 大模型直接评判：不要依赖 GPT-4 等巨额模型作为时序行为裁判，改用 7B 小模型做动作/状态的命题标注，再交由 LTL 进展自动推理，成本低且 F1 大幅度领先，适合大规模日志审计。
- 预测与干预机制降低违规率：新增预测监控模块，对即将发生的违规进行采样估计，并通过重采样、约束注入提示或切换更安全的模型进行黑盒干预，在保持任务完成率的同时显著减少违规，可嵌入到对话Agent或推荐Agent的推理循环中。
- 审计日志自动生成可解释证据：TRAC 在监控过程中记录每次公式进展的 witness，为每一步合规/违规提供可追溯的解释，便于满足监管审计要求。